A,B:es_realizer{i:l}.
R-compat{i:l}(A; B)  (i:Id. fpf-compatible(Knd; x.Type; Kind-deq; R-da(A; i); R-da(B; i))) 

latex

Definitions

ff, tt, True, T, x(s), P  Q, P  Q, P  Q, if b then t else f fi , top, x. t(x), prop{i:l}, guard(T), sq_type(T), R-da(R; i), ge(i; j), False, A, A  B, t  T, , P  Q, x:A. B(x), Unit, , P  Q, Y, R-compat{i:l}(A; B), ,

Lemmas

Rda wf, ifthenelse wf, fpf-empty wf, not functionality wrt iff, Id sq, assert-eq-id, R-loc wf, eq id wf, R-da-Rda, deq wf, true wf, squash wf, fpf-compatible wf, fpf-empty-compatible-right, top wf, fpf wf, fpf-trivial-subtype-top, fpf-empty-compatible-left, Rnone-implies, Rnone? wf, R-compat-symmetry, fpf-compatible-join, Rplus-right wf, Rplus-left wf, fpf-join wf, R-da wf, Kind-deq wf, Knd wf, fpf-compatible-symmetry, R-size-decreases, assert of bnot, eqff to assert, not wf, bnot wf, assert wf, iff transitivity, Rplus-implies, eqtt to assert, bool wf, bool sq, Rplus? wf, bool cases, ge wf, nat properties, es realizer wf, R-compat wf, Id wf, le wf, nat plus wf, R-size wf, nat wf